Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    f(cons(nil,y))  → y
2:    f(cons(f(cons(nil,y)),z))  → copy(n,y,z)
3:    copy(0,y,z)  → f(z)
4:    copy(s(x),y,z)  → copy(x,y,cons(f(y),z))
There are 4 dependency pairs:
5:    F(cons(f(cons(nil,y)),z))  → COPY(n,y,z)
6:    COPY(0,y,z)  → F(z)
7:    COPY(s(x),y,z)  → COPY(x,y,cons(f(y),z))
8:    COPY(s(x),y,z)  → F(y)
The approximated dependency graph contains one SCC: {7}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.06 seconds)   ---  May 4, 2006